structure A_Reduce =
struct
  structure A = Assert

  fun finds s =
      let fun find A.Rf = ((*print "finds Rf\n"; *)A.Rf)
            | find A.Hp = ((*print "finds Hp\n"; *)A.Hp)
            | find (A.Upd(s, e1, e2)) = ((*print "finds Upd\n"; *)finds s)
      in  find s
      end

  fun red_st s =
      let fun red A.Rf = A.Rf
            | red A.Hp = A.Hp
            | red (A.Upd(s, e1, e2)) = A.Upd(red_st s, red_exp e1, red_exp e2)
      in red s
      end

  and red_exp e =
      let fun red (A.IntNum(i)) = A.IntNum(i)
            | red (A.Addr(i)) = A.Addr(i)
	    | red (A.Plus(A.IntNum(i1), A.IntNum(i2))) = A.IntNum(i1 + i2)
	    | red (A.Plus(A.IntNum(i),e2)) = 
	      if i <> 0
	      then A.Plus(A.IntNum(i), red_exp e2) 
	      else red_exp e2
	    | red (A.Plus(e1,A.IntNum(i))) = 
	      if i <> 0
	      then A.Plus(A.IntNum(i), red_exp e1)
	      else red_exp e1
            | red (A.Plus(e1, e2)) = A.Plus(red_exp e1, red_exp e2)
            | red (A.Minus(e1, e2)) = A.Minus(red_exp e1, red_exp e2)
            | red (A.Times(e1, e2)) = A.Times(red_exp e1, red_exp e2)
            | red A.Eax = A.Eax
            | red A.Ebx = A.Ebx
            | red A.Ecx = A.Ecx            
            | red A.Edx = A.Edx
            | red A.Esi = A.Esi
            | red A.Edi = A.Edi
            | red A.Esp = A.Esp
            | red A.Ebp = A.Ebp
            | red A.Zf = A.Zf
            | red A.Sf = A.Sf
            | red (A.Sel(A.Upd(s, e1, e2), e3)) =
              ((*print "sel_upd\n";*)
               if e1 = e3
               then ((*print "eq\n"; *)red_exp e2)
               else ((*print "neq\n";*)
                     if (finds s) = A.Rf
                     then ((*print "A.Rf\n";*) red_exp (A.Sel(s, e3)))
                     else ((*print "A.Hp\n";*) A.Sel(red_st (A.Upd(s, e1, e2)), red_exp e3))))  (*WIP*)
            | red (A.Sel(s, e)) = A.Sel(s, red_exp e)
      in  red e
      end

  fun red_prop p =
      let fun red A.True = A.True
            | red (A.Imply(p1, p2)) = A.Imply(red_prop p1, red_prop p2)
            | red (A.Not(p)) = A.Not(red_prop p)
            | red (A.And(p1, p2)) = A.And(red_prop p1, red_prop p2)
            | red (A.Or(p1, p2)) = A.Or(red_prop p1, red_prop p2)
            | red (A.Gt(e1, e2)) = A.Gt(red_exp e1, red_exp e2)
            | red (A.Ge(e1, e2)) = A.Ge(red_exp e1, red_exp e2) 
            | red (A.Lt(e1, e2)) = A.Lt(red_exp e1, red_exp e2) 
            | red (A.Le(e1, e2)) = A.Le(red_exp e1, red_exp e2) 
            | red (A.Eq(e1, e2)) = A.Eq(red_exp e1, red_exp e2) 
            | red (A.Ne(e1, e2)) = A.Ne(red_exp e1, red_exp e2)
            | red (A.Ex((s, t), p)) = A.Ex((s, t), red_prop p) 
            | red (A.InDom(e, st)) = A.InDom(red_exp e, red_st st)
      in  red p
      end 

end
